feat(tg-11): epistemic types — Epi[k, ρ, τ], non-factive by construction - #98
Merged
Merged
Conversation
…ruction
Wires hyperpolymath/epistemic-types into the mechanised core, following the
route TG-10 took for echo. Lean 0 errors, sorry/axiom gate clean.
## The commitment: a warrant is not knowledge
`Epi[k, rho, tau]` = at standpoint k, evidence of type rho purporting to
support a claim of type tau. The claim type appears in the type and NO
elimination rule delivers it. `evidence` is the sole projection and yields
rho.
That mirrors upstream exactly. `Warrant.agda` gives the record only an
`Evidence` field — deliberately not `Evidence -> A`, because that "would make
every warrant factive" — and puts extraction in a separate `SoundWarrant`.
`Base.agda` likewise splits `FactiveModality` (with `reflect`) from
`BeliefModality` (without), rather than treating belief as knowledge with a
missing proof. The absence here is that same choice, mechanised.
## Six capstones
epi_evidence_recovers evidence . warrant returns the token
epi_claim_is_opaque two warrants, same evidence, DIFFERENT claims
are observationally identical — the dual of
echo_distinguishes_collapsed: echo REVEALS what
close forgot, a warrant WITHHOLDS what it
purports
epi_only_yields_evidence from Epi[k,rho,tau] the only elimination is rho
epi_distinguishes_standpoints k1 /= k2 gives different types
epi_roundtrip_typed type safety of intro + projection
epi_over_echo_typed Epi[k, Echo[rho,tau], sigma] — the two modalities
NEST; mirrors EpistemicEcho in EchoBridge.agda,
which is explicit that echo grades
irrecoverability while epi indexes standpoints
## Metatheory extended, not weakened
Progress, Preservation, Determinism, TypeSafety, infer_sound and
infer_complete all cover the new fragment. New `canonical_epi` lemma. In
preservation, the `evidenceVal` case inverts tEvidence then tEpiVal and
returns the TOKEN's typing, never the claim's — non-factivity discharged by
the type system rather than asserted.
## Both engines
OCaml mirrors it: `TEpi` former, `Warrant`/`EpiVal`/`Evidence` constructors,
`VEpi` runtime value, typing and evaluation. TG-3 extended with 4 pins
(including that `evidence` yields the evidence type, never the claim);
differential regenerated and kernel-checked — 496 obligations, 0 errors.
TG-3 self-check 1008 -> 1012.
## Registered honestly
TG-11 in PROOF-NEEDS.md; assumption A-TG-11.1 records what the simply-typed
shadow does NOT model: standpoints are Nat rather than an arbitrary index set,
the upstream functor laws / reflect / return are omitted (all opt-in there),
and — the real gap — the claim is CARRIED rather than erased, because erasing
it would break uniqueness of typing in a system without quantities. A QTT
treatment (quantity 0 on the claim) would be the faithful version.
Tests: 6 typecheck cases including two negatives — that evidence never returns
the claim type, and that `evidence` of a non-warrant is rejected. Typecheck
suite 129 -> 135; all suites green.
Co-Authored-By: Claude Opus 5 <[email protected]>
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ ApprovedIntegrates non-factive epistemic types into the mechanised core and OCaml engine, complete with six capstones and extended metatheory. No issues found.
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
|
|
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
hyperpolymath
added a commit
that referenced
this pull request
Jul 29, 2026
…ent-order bug (#99) TG-11 (#98) landed the type former, typing, evaluation and six proofs — but there was **no way to write one**. Zero occurrences of the constructors in `lexer.mll` or `parser.mly`, against 4 for echo. Fully implemented and unreachable. ## Surface syntax ```tangle def w = warrant[0](42, braid[s1, s2]) -- at standpoint 0 def token = evidence(w) -- the ONLY elimination ``` The standpoint is bracketed because it's an *index*, not an operand — the same reading as a braid generator's subscript. No grammar conflicts. **Non-factivity reaches the syntax.** There is deliberately no keyword extracting the claim: `claim(w)` parses as an ordinary call to an undefined function, never as a language form. A test pins that distinction — if a `Claim` form ever appears, it contradicts `epi_only_yields_evidence`. ## A *second* copy of the statement-order bug Writing the first epistemic program surfaced it immediately: ``` def w = warrant[0](42, braid[s1]) def tok = evidence(w) → In definition 'tok': evidence requires an Epi[k, rho, tau], got Word[0] ``` That `Word[0]` is the pass-1a **placeholder** — `tok` was being checked *before* `w` was refined. Same root cause as #95 (`stmts := prog @ !stmts` then `List.rev` on the flattened list), but in a **second copy**, in `lib/check.ml`. **That copy feeds `tanglec --check` and the LSP.** Both have been analysing programs with their statements reversed. And it was never epistemic-specific: ``` def e = echoClose(braid[s1]) def r = residue(e) → residue requires Echo[_, _], got Word[0] ``` **Any cross-definition reference to a non-`Word` type was mis-typed.** Echo has been broken this way for as long as the recovering path has existed. The test suites missed *both* copies for the same reason: they call `Parser.program` directly and never exercise the recovering path. ## Tests **Parser** — warrant with bracketed standpoint; evidence; TG-4 round-trip; the no-claim-form guard. **Check** — three cross-definition cases (plain, echo, epistemic), all of which would have failed before this. ## Example `examples/epistemic.tangle`, wired into the corpus gate's must-run set — warrants at three standpoints, evidence recovery, and the echo composition `residue(evidence(we))`. All assertions pass. It also documents *why* the claim is unreachable: if it were extractable, anything anyone attested would become true by fiat — precisely the bug you don't want in a provenance system. All gates green: Lean 0 errors, full suite, corpus, RSR. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5 <[email protected]>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Wires
hyperpolymath/epistemic-typesinto the mechanised core, following the route TG-10 took for echo. Lean 0 errors, sorry/axiom gate clean.The commitment: a warrant is not knowledge
Epi[κ, ρ, τ]— at standpoint κ, evidence of type ρ purporting to support a claim of type τ. The claim type appears in the type and no elimination rule delivers it.evidenceis the sole projection, and it yields ρ.That mirrors upstream precisely:
Warrant.agdagives the record only anEvidencefield — deliberately notEvidence → A, because that "would make every warrant factive" — and puts extraction in a separateSoundWarrant.Base.agdasplitsFactiveModality(withreflect : E κ A → A) fromBeliefModality(without), rather than treating belief as knowledge with a missing proof.The absence here is that same design choice, mechanised.
Six capstones
epi_evidence_recoversevidence ∘ warrantreturns the tokenepi_claim_is_opaqueepi_only_yields_evidenceEpi[κ,ρ,τ]the only elimination is at ρepi_distinguishes_standpointsepi_roundtrip_typedepi_over_echo_typedEpi[κ, Echo[ρ,τ], σ]— the modalities nestepi_claim_is_opaqueis the exact dual ofecho_distinguishes_collapsed: echo reveals whatcloseforgot; a warrant withholds what it purports. Holding evidence is not holding the fact.epi_over_echo_typedmirrorsEpistemicEchoinEchoBridge.agda, which is explicit that these are different modalities — echo grades irrecoverability, epi indexes standpoints — and that they compose without collapsing.Metatheory extended, not weakened
Progress, Preservation, Determinism, TypeSafety,
infer_sound,infer_completeall cover the new fragment, plus a newcanonical_epilemma.Worth noting where non-factivity actually lands: in preservation, the
evidenceValcase invertstEvidencethentEpiValand returns the token's typing (he), never the claim's (hc). Non-factivity is discharged by the type system rather than asserted in a comment.Both engines
OCaml mirrors it —
TEpiformer,Warrant/EpiVal/Evidence,VEpiruntime value, typing and evaluation. TG-3 extended with 4 pins (including thatevidenceyields the evidence type, never the claim); differential regenerated and kernel-checked: 496 obligations, 0 errors. TG-3 self-check 1008 → 1012.⚠ Registered honestly — A-TG-11.1
What the simply-typed shadow does not model:
Nat, not an arbitrary index setK;LawfulModalityfunctor laws,FactiveModality.reflectandReturnModality.returnare omitted (all opt-in there);A QTT treatment (quantity
0on the claim) would be the faithful version — which is the same conclusion the linear/affine discussion reached independently.Tests
6 typecheck cases, including two negatives: that
evidencenever returns the claim type when the two differ, and thatevidenceof a non-warrant is rejected. Typecheck suite 129 → 135; all suites green; corpus and RSR gates pass.🤖 Generated with Claude Code